gmanager

Makefile.in

@@ -262,36 +262,53 @@ install::
 	cp -f bin/whyml.@OCAMLBEST@ $(BINDIR)/whyml3
 
 ###############
-# proof manager
+# rust prover
 ###############
 
-MNG_FILES = db scheduler test
+MNG_FILES = db scheduler 
+MNG_MAIN_FILES = test gmanager
 
 MNGMODULES = $(addprefix src/manager/, $(MNG_FILES))
+MNGMAINS = $(addprefix src/manager/, $(MNG_MAIN_FILES))
 
 MNGML  = $(addsuffix .ml,  $(MNGMODULES))
 MNGMLI = $(addsuffix .mli, $(MNGMODULES))
 MNGCMO = $(addsuffix .cmo, $(MNGMODULES))
 MNGCMX = $(addsuffix .cmx, $(MNGMODULES))
 
-$(MNGCMO) $(MNGCMX): INCLUDES = -thread -I src/manager -I +sqlite3 
+$(MNGCMO) $(MNGCMX) $(addsuffix .cmx, $(MNGMAINS)) $(addsuffix .cmo, $(MNGMAINS)): INCLUDES = -thread -I src/manager -I +sqlite3 -I +threads
 
-ifeq (@enable_proof_manager@,yes)
-byte: bin/manager.byte
-opt:  bin/manager.opt
+src/manager/gmanager.cmo src/manager/gmanager.cmx: INCLUDES += -I +lablgtk2
+
+ifeq (@enable_rust_prover@,yes)
+byte: bin/manager-test.byte bin/why-rustprover.byte
+opt:  bin/manager-test.opt bin/why-rustprover.opt
 endif
 
-bin/manager.opt bin/manager.byte: INCLUDES = -thread -I +sqlite3
+bin/manager-test.opt bin/manager-test.byte: INCLUDES = -thread -I +sqlite3
 
-bin/manager.opt: src/why.cmxa $(MNGCMX)
+bin/manager-test.opt: src/why.cmxa $(MNGCMX) src/manager/test.cmx
 	$(if $(QUIET), @echo 'Linking  $@' &&) \
 	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa sqlite3.cmxa $^
 	$(STRIP) $@
 
-bin/manager.byte: src/why.cma $(MNGCMO)
+bin/manager-test.byte: src/why.cma $(MNGCMO) src/manager/test.cmo
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
 	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma sqlite3.cma $^
 
+bin/why-rustprover.opt bin/why-rustprover.byte: INCLUDES = -thread -I +sqlite3 -I +lablgtk2
+
+bin/why-rustprover.opt: src/why.cmxa $(MNGCMX) src/manager/gmanager.cmx
+	$(if $(QUIET), @echo 'Linking  $@' &&) \
+	    $(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) threads.cmxa \
+	lablgtk.cmxa lablgtksourceview2.cmxa gtkThread.cmx sqlite3.cmxa $^
+	$(STRIP) $@
+
+bin/why-rustprover.byte: src/why.cma $(MNGCMO) src/manager/gmanager.cmo
+	$(if $(QUIET),@echo 'Linking  $@' &&) \
+	    $(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) threads.cma \
+	lablgtk.cma lablgtksourceview2.cma gtkThread.cmo sqlite3.cma $^
+
 # depend and clean targets
 
 include .depend.manager

configure.in

@@ -59,11 +59,11 @@ AC_ARG_ENABLE(verbose-make,
     [  --enable-verbose-make   verbose makefile commands],,
     enable_verbose_make=no)
 
-# proof manager
+# rust prover
 
-AC_ARG_ENABLE(proof-manager,
-    [  --enable-proof-manager  enable Why3 proof manager],,
-    enable_proof_manager=yes)
+AC_ARG_ENABLE(rust-prover,
+    [  --enable-rust-prover  enable Why3 rust prover],,
+    enable_rust_prover=yes)
 
 # IDE
 
@@ -220,8 +220,8 @@ fi
 AC_CHECK_PROG(CAMLP5O,camlp5o,camlp5o,no)
 
 # checking for sqlite3
-if test "$enable_proof_manager" = yes ; then
-AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_proof_manager=no)
+if test "$enable_rust_prover" = yes ; then
+AC_CHECK_FILE($OCAMLLIB/sqlite3/sqlite3.cma,,enable_rust_prover=no)
 fi
 
 # checking for lablgtk2
@@ -316,7 +316,7 @@ dnl AC_SUBST(OCAMLWEB)
 AC_SUBST(CAMLP5O)
 
 AC_SUBST(enable_ide)
-AC_SUBST(enable_proof_manager)
+AC_SUBST(enable_rust_prover)
 AC_SUBST(enable_plugins)
 AC_SUBST(DYNLINK)
 
@@ -351,7 +351,7 @@ echo "OCaml library path      : $OCAMLLIB"
 echo "Verbose make            : $enable_verbose_make"
 echo "Why IDE                 : $enable_ide"
 echo "Why plugins             : $enable_plugins"
-echo "Why proof manager       : $enable_proof_manager"
+echo "Why rust prover         : $enable_rust_prover"
 echo "Coq support             : $enable_coq_support"
 if test "$enable_coq_support" = "yes" ; then
    echo "    Version             : $COQVERSION"

src/manager/gmanager.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  Copyright (C) 2010-                                                   *)
+(*    Francois Bobot                                                      *)
+(*    Jean-Christophe Filliatre                                           *)
+(*    Johannes Kanig                                                      *)
+(*    Andrei Paskevich                                                    *)
+(*                                                                        *)
+(*  This software is free software; you can redistribute it and/or        *)
+(*  modify it under the terms of the GNU Library General Public           *)
+(*  License version 2.1, with the special exception on linking            *)
+(*  described in file LICENSE.                                            *)
+(*                                                                        *)
+(*  This software is distributed in the hope that it will be useful,      *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+let pname = "[Why-rustprover]"
+
+let () = ignore (GtkMain.Main.init ())
+
+open Format
+open Why
+open Whyconf
+
+(******************************)
+(* loading user configuration *)
+(******************************)
+
+let config = 
+  try 
+    Whyconf.read_config None
+  with 
+      Not_found -> 
+        eprintf "%s No config file found.@." pname;
+        exit 1
+    | Whyconf.Error e ->
+        eprintf "%s Error while reading config file: %a@." pname 
+          Whyconf.report e;
+        exit 1
+
+let () = eprintf "%s Load path is: %a@." pname
+  (Pp.print_list Pp.comma Pp.string) config.loadpath
+
+let timelimit = 
+  match config.timelimit with
+    | None -> 2
+    | Some n -> n
+
+
+(* TODO: put that in config file *)
+let window_width = 1024
+let window_height = 768
+let font_name = "Monospace 10"
+
+let spec = []
+let usage_str = "why-rustprover [options] <file>.why"
+let file = ref None
+let set_file f = match !file with
+  | Some _ -> 
+      raise (Arg.Bad "only one file")
+  | None -> 
+      if not (Filename.check_suffix f ".why") then 
+	raise (Arg.Bad ("don't know what to do with " ^ f));
+      if not (Sys.file_exists f) then begin
+	Format.eprintf "%s %s: no such file@." pname f; 
+        exit 1
+      end;
+      file := Some f
+
+let () = Arg.parse spec set_file usage_str
+
+let fname = match !file with
+  | None -> 
+      Arg.usage spec usage_str; 
+      exit 1
+  | Some f -> 
+      f
+
+let lang =
+  let load_path = 
+    List.fold_right Filename.concat 
+      [Filename.dirname Sys.argv.(0); ".."; "share"] "lang" 
+  in
+  let languages_manager = 
+    GSourceView2.source_language_manager ~default:true 
+  in
+  languages_manager#set_search_path 
+    (load_path :: languages_manager#search_path);
+  match languages_manager#language "why" with
+    | None -> Format.eprintf "pas trouv@;"; None
+    | Some _ as l -> l
+
+let source_text = 
+  let ic = open_in fname in
+  let size = in_channel_length ic in
+  let buf = String.create size in
+  really_input ic buf 0 size;
+  close_in ic;
+  buf
+
+let env = Why.Env.create_env (Why.Typing.retrieve config.loadpath)
+
+
+(***********************)
+(* Parsing input file  *)
+(***********************)
+   
+let rec report fmt = function
+  | Lexer.Error e ->
+      fprintf fmt "lexical error: %a" Lexer.report e;
+  | Loc.Located (loc, e) ->
+      fprintf fmt "%a%a" Loc.report_position loc report e
+  | Parsing.Parse_error ->
+      fprintf fmt "syntax error"
+  | Denv.Error e ->
+      Denv.report fmt e
+  | Typing.Error e ->
+      Typing.report fmt e
+  | Decl.UnknownIdent i ->
+      fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_string
+  | Driver.Error e ->
+      Driver.report fmt e
+  | Config.Dynlink.Error e ->
+      fprintf fmt "Dynlink : %s" (Config.Dynlink.error_message e)
+  | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
+
+
+let theories : Theory.theory Theory.Mnm.t =
+  try
+    let cin = open_in fname in
+    let m = Env.read_channel env fname cin in
+    close_in cin;
+    eprintf "Parsing/Typing Ok@.";
+    m
+  with e -> 
+    eprintf "%a@." report e;
+    exit 1
+
+(********************)
+(* opening database *)
+(********************)
+
+let () = Db.init_base (fname ^ ".db")
+
+let get_driver name = 
+  let pi = Util.Mstr.find name config.provers in
+  Why.Driver.load_driver env pi.Whyconf.driver
+
+type prover_data =
+    { prover : Db.prover;
+      command : string;
+      driver : Why.Driver.driver;
+    }
+
+let provers_data =
+  printf "===============================@\nProvers: ";
+  let l = 
+    Util.Mstr.fold
+    (fun id conf acc ->
+       let name = conf.Whyconf.name in
+       printf " %s, " name;
+       { prover = Db.get_prover name;
+         command = conf.Whyconf.command;
+         driver = get_driver id; } :: acc
+    ) config.provers []
+  in
+  printf "@\n===============================@.";
+  l 
+   
+let () = 
+  printf "previously known goals:@\n";
+  List.iter (fun s -> printf "%s@\n" (Db.goal_task_checksum s)) (Db.root_goals ());
+  printf "@."
+
+
+(***************************)
+(* Process input theories  *)
+(* add corresponding tasks *)
+(***************************)
+
+let add_task (tname : string) (task : Why.Task.task) acc =
+  let name = (Why.Task.task_goal task).Why.Decl.pr_name.Why.Ident.id_string in
+  eprintf "doing task: tname=%s, name=%s@." tname name;
+  Db.add_or_replace_task ~tname ~name task :: acc
+
+let do_theory tname th glist =
+  let tasks = Why.Task.split_theory th None in
+  List.fold_right (add_task tname) tasks glist
+
+
+(****************)
+(* goals widget *)
+(****************)
+
+module Ide_goals = struct
+
+  let cols = new GTree.column_list
+  let column = cols#add Gobject.Data.string
+
+  let renderer = GTree.cell_renderer_text [`XALIGN 0.] 
+  let vcolumn = 
+    GTree.view_column ~title:"Goals" 
+      ~renderer:(renderer, ["text", column]) () 
+
+  let () = 
+    vcolumn#set_resizable true;
+    vcolumn#set_max_width 400
+
+  let create ~packing () =
+    let model = GTree.tree_store cols in
+    let view = GTree.view ~model ~packing () in
+    let _ = view#selection#set_mode `SINGLE in
+    let _ = view#set_rules_hint true in
+    ignore (view#append_column vcolumn);
+    model
+
+  let clear model = model#clear ()
+
+  let add_goals (model : GTree.tree_store) th =
+    let rec fill parent ns =
+      let add_s k s _ = 
+	let row = model#append ~parent () in
+	model#set ~row ~column (k ^ s)
+      in
+(*
+      Mnm.iter (add_s "type ")  ns.ns_ts;
+      Mnm.iter (add_s "logic ") ns.ns_ls;
+*)
+      Theory.Mnm.iter (add_s "prop ")  ns.Theory.ns_pr;
+(*
+      let add_ns s ns =
+	let row = model#append ~parent () in
+	model#set ~row ~column s;
+	fill row ns
+      in
+      Mnm.iter add_ns ns.ns_ns
+*)
+    in
+    let row = model#append () in
+    model#set ~row ~column (th.Theory.th_name.Ident.id_string : string);
+    fill row th.Theory.th_export
+
+end
+
+
+(* windows, etc *)
+
+let main () =
+  let w = GWindow.window 
+    ~allow_grow:true ~allow_shrink:true
+    ~width:window_width ~height:window_height 
+    ~title:"why-ide" ()
+  in
+  let _ = w#connect#destroy ~callback:(fun () -> exit 0) in
+  let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
+
+  (* Menu *)
+  let menubar = GMenu.menu_bar ~packing:vbox#pack () in
+  let factory = new GMenu.factory menubar in
+  let accel_group = factory#accel_group in
+  let file_menu = factory#add_submenu "_File" in
+  let file_factory = new GMenu.factory file_menu ~accel_group in
+  let _ = 
+    file_factory#add_image_item ~key:GdkKeysyms._Q ~label:"_Quit" 
+      ~callback:(fun () -> exit 0) () 
+  in
+
+  (* horizontal paned *)
+  let hp = GPack.paned `HORIZONTAL  ~border_width:3 ~packing:vbox#add () in
+
+  (* left tree of namespace *)
+  let scrollview = 
+    GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC 
+    ~width:(window_width / 3) ~packing:hp#add () 
+  in
+  let _ = scrollview#set_shadow_type `ETCHED_OUT in
+
+  let goals_view = Ide_goals.create ~packing:scrollview#add () in
+  Theory.Mnm.iter (fun _ th -> Ide_goals.add_goals goals_view th) theories;
+
+  (* source view *)
+  let scrolled_win = GBin.scrolled_window
+    ~hpolicy: `AUTOMATIC ~vpolicy: `AUTOMATIC
+    ~packing:hp#add ()
+  in
+  let source_view =
+    GSourceView2.source_view
+      ~auto_indent:true
+      ~insert_spaces_instead_of_tabs:true ~tab_width:2
+      ~show_line_numbers:true
+      ~right_margin_position:80 ~show_right_margin:true
+      (* ~smart_home_end:true *)
+      ~packing:scrolled_win#add ~height:500 ~width:650
+      ()
+  in
+  source_view#misc#modify_font_by_name font_name;
+  source_view#source_buffer#set_language lang;
+  source_view#set_highlight_current_line true;
+  source_view#source_buffer#set_text source_text;
+ 
+  w#add_accel_group accel_group;
+  w#show ()
+
+let () =
+  main ();
+  GtkThread.main ()
+
+(*
+Local Variables: 
+compile-command: "unset LANG; make -C ../.. bin/whyide.opt"
+End: 
+*)

src/manager/test.ml

@@ -78,7 +78,7 @@ let config =
 
 let () = printf "Load path is: %a@." (Pp.print_list Pp.comma Pp.string) config.loadpath
 
-let env = Why.Env.create_env (Why.Typing.retrieve config.loadpath)
+let env = Env.create_env (Typing.retrieve config.loadpath)
 
 let timelimit = 
   match config.timelimit with
@@ -95,12 +95,12 @@ let () = Db.init_base (fname ^ ".db")
 
 let get_driver name = 
   let pi = Util.Mstr.find name config.provers in
-  Why.Driver.load_driver env pi.Whyconf.driver
+  Driver.load_driver env pi.Whyconf.driver
 
 type prover_data =
     { prover : Db.prover;
       command : string;
-      driver : Why.Driver.driver;
+      driver : Driver.driver;
     }
 
 let provers_data =
@@ -147,10 +147,10 @@ let rec report fmt = function
   | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
 
 
-let m : Why.Theory.theory Why.Theory.Mnm.t =
+let m : Theory.theory Theory.Mnm.t =
   try
     let cin = open_in (fname ^ ".why") in
-    let m = Why.Env.read_channel env fname cin in
+    let m = Env.read_channel env fname cin in
     close_in cin;
     eprintf "Parsing/Typing Ok@.";
     m
@@ -163,13 +163,13 @@ let m : Why.Theory.theory Why.Theory.Mnm.t =
 (* add corresponding tasks *)
 (***************************)
 
-let add_task (tname : string) (task : Why.Task.task) acc =
-  let name = (Why.Task.task_goal task).Why.Decl.pr_name.Why.Ident.id_string in
+let add_task (tname : string) (task : Task.task) acc =
+  let name = (Task.task_goal task).Decl.pr_name.Ident.id_string in
   eprintf "doing task: tname=%s, name=%s@." tname name;
   Db.add_or_replace_task ~tname ~name task :: acc
 
 let do_theory tname th glist =
-  let tasks = Why.Task.split_theory th None in
+  let tasks = Task.split_theory th None in
   List.fold_right (add_task tname) tasks glist
 
 
@@ -267,15 +267,15 @@ let main_loop goals =
 let () =
   eprintf "looking for goals@.";
   let add_th t th mi = 
-    eprintf "adding theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_string t;
-    Why.Ident.Mid.add th.Why.Theory.th_name (t,th) mi 
+    eprintf "adding theory %s, %s@." th.Theory.th_name.Ident.id_string t;
+    Ident.Mid.add th.Theory.th_name (t,th) mi 
   in
   let do_th _ (t,th) glist = 
-    eprintf "doing theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_string t;
+    eprintf "doing theory %s, %s@." th.Theory.th_name.Ident.id_string t;
     do_theory t th glist  
   in
   let goals = 
-    Why.Ident.Mid.fold do_th (Why.Theory.Mnm.fold add_th m Why.Ident.Mid.empty) []
+    Ident.Mid.fold do_th (Theory.Mnm.fold add_th m Ident.Mid.empty) []
   in
   eprintf "Production of goals done@.";
   try