manager

Makefile.in

@@ -82,7 +82,7 @@ all: @OCAMLBEST@
 # Why library 
 #############
 
-LIBGENERATED = src/config.ml \
+LIBGENERATED = src/config.ml src/util/rc.ml \
           src/parser/parser.mli src/parser/parser.ml src/parser/parser.output \
             src/parser/lexer.ml src/driver/driver_lexer.ml \
             src/driver/driver_parser.mli src/driver/driver_parser.ml \
@@ -111,7 +111,7 @@ CORE_CMO := ident.cmo ty.cmo term.cmo pattern.cmo decl.cmo theory.cmo\
 CORE_CMO := $(addprefix src/core/,$(CORE_CMO))
 
 UTIL_CMO := pp.cmo loc.cmo prtree.cmo util.cmo hashcons.cmo \
-            sysutil.cmo hashweak.cmo
+            sysutil.cmo hashweak.cmo rc.cmo
 UTIL_CMO := $(addprefix src/util/,$(UTIL_CMO))
 
 PARSER_CMO := ptree.cmo parser.cmo lexer.cmo denv.cmo typing.cmo 
@@ -125,7 +125,7 @@ TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 
 DRIVER_CMO := driver_ast.cmo call_provers.cmo dynlink_compat.cmo \
-              driver_parser.cmo driver_lexer.cmo whyrc.cmo driver.cmo
+              driver_parser.cmo driver_lexer.cmo driver.cmo whyrc.cmo 
 DRIVER_CMO := $(addprefix src/driver/,$(DRIVER_CMO))
 
 PRINTER_CMO := print_real.cmo alt_ergo.cmo why3.cmo smt.cmo coq.cmo
@@ -230,19 +230,6 @@ clean::
 # proof manager
 ###############
 
-src/orm/sql_orm_header.ml: src/orm/sql_access.ml src/orm/convert.ml 
-	ocaml src/orm/convert.ml $< $@
-
-ORM_CMO := printer_utils.cmo sql_orm_header.cmo sql_orm.cmo
-ORM_CMO := $(addprefix src/orm/,$(ORM_CMO))
-
-$(ORM_CMO): INCLUDES=-I src/orm -I +sqlite3
-
-# src/manager/db.ml: $(ORM_CMO) src/manager/orm_schema.ml
-# 	ocaml -I src/orm src/manager/orm_schema.ml 
-
-src/manager/orm_schema.ml: $(ORM_CMO)
-
 MANAGER_CMO := db.cmo test.cmo
 MANAGER_CMO := $(addprefix src/manager/,$(MANAGER_CMO))
 

src/driver/whyrc.ml

 
-
+open Format
 
 let default_why3rc_file () = 
-  let home = 
-    try Sys.getenv "HOME"
-    with Not_found -> 
-      (* try windows env var *)
-      try Sys.getenv "USERPROFILE"
-      with Not_found -> ""
-  in
-  Filename.concat (Filename.concat home ".why") "why3rc"
+  let home = Rc.get_home_dir () in
+  let dir = Filename.concat home ".why" in
+  (* TODO: create dir if not exists *)
+  Filename.concat dir "why3rc"
 
-let read_config_file ?(name = default_why3rc_file()) =
-  assert false (* TODO *)
+let known_provers : (string, string * Driver.driver option ref) Hashtbl.t = 
+  Hashtbl.create 7  
 
+let load_prover_info info =
+  let name = ref "" in
+  let driv = ref "" in
+  List.iter
+    (function 
+       | ("name",Rc.RCstring s) -> name := s
+       | ("driver",Rc.RCstring s) -> driv := s
+       | (field,_) ->
+	   eprintf 
+	     "Warning: ignored field `%s' in section [prover] of rc file@." 
+	     field)
+    info;
+  Hashtbl.add known_provers !name (!driv,ref None)
 
-let known_provers () = 
-  assert false (* TODO *)
+let config_file = ref ""
 
-let get_driver name env = 
-  assert false (* TODO *)
+let read_config_file ?(name = default_why3rc_file()) () =
+  if !config_file <> "" then begin
+    eprintf "Whyrc.read_config_file: cannot load config file twice@.";
+    exit 2;
+  end;
+  config_file := name;
+  let rc = Rc.from_file name in
+  List.iter
+    (fun (key,args) ->
+       match key with
+	 | "prover" -> load_prover_info args
+	 | _ -> 
+	     eprintf 
+	       "Warning: ignored section [%s] in config file '%s'@." key name)
+    rc
 
+let get_driver name env = 
+  if !config_file = "" then begin
+    eprintf "Whyrc.get_driver: config file not loaded yet@.";
+    exit 2;
+  end;
+  let (file,driv) = Hashtbl.find known_provers name in
+  match !driv with
+    | Some d -> d
+    | None ->
+	let d = Driver.load_driver file env in
+	driv := Some d;
+	d
 
 let add_driver_config id file cmd =
-  assert false (* TODO *)
-
+    (* TODOL the command [cmd] should be inserted in the template [file] 
+       and the result copied into ".why/<id>.drv" 
+       corresponding values must be added into [known_provers]
+    *)
+  Hashtbl.add known_provers id (file, ref None)
+       
 let save () =
-  assert false (* TODO *)
+  if !config_file = "" then begin
+    eprintf "Whyrc.save: config file not loaded yet@.";
+    exit 2;
+  end;
+  let ch = open_out !config_file in
+  let fmt = Format.formatter_of_out_channel ch in
+  Hashtbl.iter
+    (fun name (driv,_) -> 
+       fprintf fmt "[prover]@.";
+       fprintf fmt "name = \"%s\"@." name;
+       fprintf fmt "driver = \"%s\"@." driv;
+       fprintf fmt "@.")
+    known_provers;
+  close_out ch
+
+    
+let known_provers () = 
+  Hashtbl.fold (fun key _ acc -> key::acc) known_provers []
+

src/driver/whyrc.mli

@@ -3,7 +3,7 @@
 
 (** {2 access to user configuration and drivers} *)
 
-val read_config_file: ?name:string -> unit
+val read_config_file: ?name:string -> unit -> unit
   (** reads the config file from file [name]. The
       default rc file name is "$HOME/.why/why3rc" if HOME is set, or
       "$USERPROFILE/.why/why3rc" if USERPROFILE is set, or "./.why/why3rc"
@@ -13,7 +13,8 @@ val known_provers: unit -> string list
   (** returns the list of known prover ids. *)
 
 val get_driver: string -> Env.env -> Driver.driver
-  (** returns the driver associated to the given prover id *)
+  (** returns the driver associated to the given prover id 
+      @raises Not_found if no driver of this name exist *)
 
 
 (** {2 configuration update} *)

src/manager/test.ml

+
+open Why
+
+let autodetection () = 
+  Whyrc.add_driver_config "Alt-Ergo 0.9" "drivers/alt_ergo.drv" "alt-ergo";
+  Whyrc.add_driver_config "Z3 2.2" "drivers/z3.drv" "z3";
+  Whyrc.add_driver_config "CVC3 2.1" "drivers/cvc3.drv" "cvc3";
+  Whyrc.add_driver_config "Coq 8.3" "drivers/coq.drv" "coqc";
+  Whyrc.save ()
+
+let () = 
+  try Whyrc.read_config_file ()
+  with Not_found -> 
+    Format.eprintf "No whyrc file found. Running autodetection of provers.@.";
+    autodetection ()
+
+
+
+    
+
+
+

src/util/rc.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  The Why platform for program certification                            *)
+(*  Copyright (C) 2002-2008                                               *)
+(*    Romain BARDOU                                                       *)
+(*    Jean-François COUCHOT                                               *)
+(*    Mehdi DOGGUY                                                        *)
+(*    Jean-Christophe FILLIÂTRE                                           *)
+(*    Thierry HUBERT                                                      *)
+(*    Claude MARCHÉ                                                       *)
+(*    Yannick MOY                                                         *)
+(*    Christine PAULIN                                                    *)
+(*    Yann RÉGIS-GIANAS                                                   *)
+(*    Nicolas ROUSSET                                                     *)
+(*    Xavier URBAIN                                                       *)
+(*                                                                        *)
+(*  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, 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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+type rc_value =
+  | RCint of int
+  | RCbool of bool
+  | RCfloat of float
+  | RCstring of string
+  | RCident of string
+
+val int : rc_value -> int
+  (** raise Failure "Rc.int" if not a int value *)
+
+val bool : rc_value -> bool
+  (** raise Failure "Rc.bool" if not a int value *)
+
+val string : rc_value -> string
+  (** raise Failure "Rc.string" if not a string or an ident value *)
+
+val from_file : string -> (string * (string * rc_value) list) list
+  (** returns the records of the file [f]
+      @raises Not_found is f does not exists 
+      @raises Failure "lexing" in case of incorrect syntax *)
+
+val get_home_dir : unit -> string
+  (** returns the home dir of the user *)
+
+

src/util/rc.mll

+(**************************************************************************)
+(*                                                                        *)
+(*  The Why platform for program certification                            *)
+(*  Copyright (C) 2002-2008                                               *)
+(*    Romain BARDOU                                                       *)
+(*    Jean-Franois COUCHOT                                               *)
+(*    Mehdi DOGGUY                                                        *)
+(*    Jean-Christophe FILLITRE                                           *)
+(*    Thierry HUBERT                                                      *)
+(*    Claude MARCH                                                       *)
+(*    Yannick MOY                                                         *)
+(*    Christine PAULIN                                                    *)
+(*    Yann RGIS-GIANAS                                                   *)
+(*    Nicolas ROUSSET                                                     *)
+(*    Xavier URBAIN                                                       *)
+(*                                                                        *)
+(*  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, 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.                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+{
+
+  open Lexing
+
+  let get_home_dir () =
+    try Sys.getenv "HOME"
+    with Not_found -> 
+      (* try windows env var *)
+      try Sys.getenv "USERPROFILE"
+      with Not_found -> ""
+
+type rc_value =
+  | RCint of int
+  | RCbool of bool
+  | RCfloat of float
+  | RCstring of string
+  | RCident of string
+
+let int = function
+  | RCint n -> n
+  | _ -> failwith "Rc.int"
+
+let bool = function
+  | RCbool b -> b
+  | _ -> failwith "Rc.bool"
+
+let string = function
+  | RCident s | RCstring s -> s
+  | _ -> failwith "Rc.string"
+
+let buf = Buffer.create 17
+
+let current_rec = ref ""
+let current_list = ref []
+let current = ref []
+
+let push_field key value =
+  current_list := (key,value) :: !current_list
+
+let push_record () =
+  if !current_list <> [] then
+    current := (!current_rec,List.rev !current_list) :: !current;
+  current_rec := "";
+  current_list := []
+
+}
+
+let space = [' ' '\t' '\r' '\n']+
+let digit = ['0'-'9']
+let letter = ['a'-'z' 'A'-'Z']
+let ident = (letter | '_') (letter | digit | '_' | '-' | '(' | ')') * 
+let sign = '-' | '+' 
+let integer = sign? digit+
+let mantissa = ['e''E'] sign? digit+
+let real = sign? digit* '.' digit* mantissa?
+let escape = ['\\''"''n''t''r']
+
+rule record = parse
+  | space 
+      { record lexbuf }
+  | '[' (ident as key) ']'  
+      { push_record();
+	current_rec := key;
+	record lexbuf 
+      }
+  | eof 
+      { push_record () }
+  | (ident as key) space* '=' space* 
+      { value key lexbuf }
+  | _ as c
+      { failwith ("Rc: invalid keyval pair starting with " ^ String.make 1 c) }
+
+and value key = parse
+  | integer as i
+      { push_field key (RCint (int_of_string i));
+        record lexbuf }
+  | real as r
+      { push_field key (RCfloat (float_of_string r));
+        record lexbuf }
+  | '"' 
+      { Buffer.clear buf;
+	string_val key lexbuf } 
+  | "true"
+      { push_field key (RCbool true);
+        record lexbuf }
+  | "false"
+      { push_field key (RCbool false);
+        record lexbuf }
+  | ident as id
+      { push_field key (RCident (*kind_of_ident*) id);
+        record lexbuf }
+  | _ as c
+      { failwith ("Rc: invalid value starting with " ^ String.make 1 c) }
+  | eof
+      { failwith "Rc: unterminated keyval pair" }
+
+and string_val key = parse 
+  | '"' 
+      { push_field key (RCstring (Buffer.contents buf));
+	record lexbuf
+      }
+  | [^ '\\' '"'] as c
+      { Buffer.add_char buf c;
+        string_val key lexbuf }
+  | '\\' (['\\''\"'] as c)   
+      { Buffer.add_char buf c;
+        string_val key lexbuf }
+  | '\\' 'n'
+      { Buffer.add_char buf '\n';
+        string_val key lexbuf }
+  | '\\' (_ as c)
+      { Buffer.add_char buf '\\';
+        Buffer.add_char buf c;
+        string_val key lexbuf }
+  | eof
+      { failwith "Rc: unterminated string" }
+
+
+{
+
+  let from_file f =
+      let c = 
+	try open_in f 
+	with Sys_error _ -> raise Not_found
+(*
+	  Format.eprintf "Cannot open file %s@." f;
+	  exit 1
+*)
+      in
+      current := [];
+      let lb = from_channel c in
+      record lb;
+      close_in c;
+      List.rev !current
+
+}