refactorisation of rc, whyconf, gconfig

src/coq-plugin/whytac.ml

@@ -41,10 +41,12 @@ let debug =
   with Not_found -> false
 
 let config = Whyconf.read_config None
+let main = Whyconf.get_main config
+let cprovers = Whyconf.get_provers config
 
-let timelimit = config.main.timelimit
+let timelimit = main.timelimit
 
-let env = Env.create_env (Lexer.retrieve config.main.loadpath)
+let env = Env.create_env (Lexer.retrieve main.loadpath)
     
 let provers = Hashtbl.create 17
 
@@ -52,7 +54,7 @@ let get_prover s =
   try 
     Hashtbl.find provers s 
   with Not_found -> 
-    let cp = Util.Mstr.find s config.provers in
+    let cp = Util.Mstr.find s cprovers in
     let drv = Driver.load_driver env cp.driver in
     Hashtbl.add provers s (cp, drv);
     cp, drv

src/driver/whyconf.mli

@@ -41,20 +41,9 @@ type main = {
   (* max number of running prover processes *)
 }
 
-type ide = {
-  window_width : int;
-  window_height : int;
-  tree_width : int;
-  task_height : int;
-  verbose : int;
-  default_editor : string;
-}
-
 type config = {
   conf_file : string;       (* "/home/innocent_user/.why.conf" *)
-  provers   : config_prover Mstr.t;   (* indexed by short identifiers *)
-  main      : main;
-  ide       : ide;
+  config    : Rc.t;
 }
 
 val default_config : config
@@ -66,5 +55,12 @@ val read_config : string option -> config
 
 val save_config : config -> unit
 
+val get_main    : config  -> main
+val get_provers : config  -> config_prover Mstr.t
+
+val set_main    : config -> main                 -> config
+val set_provers : config -> config_prover Mstr.t -> config
+
+
 (** Replace the provers by autodetected one *)
-val run_auto_detection : config -> config
+val run_auto_detection : unit -> config_prover Mstr.t

src/ide/gconfig.ml

@@ -3,6 +3,7 @@ open Format
 open Why
 open Util
 open Whyconf
+open Rc
 
 type prover_data =
     { prover_id : string;
@@ -29,20 +30,40 @@ type t =
       mutable config : Whyconf.config;
     }
 
-let load_main c (key, value) =
-  match key with
-    | "width" -> c.window_width <- Rc.int value
-    | "height" -> c.window_height <- Rc.int value
-    | "tree_width" -> c.tree_width <- Rc.int value
-    | "task_height" -> c.task_height <- Rc.int value
-    | "time_limit" -> c.time_limit <- Rc.int value
-    | "verbose" -> c.verbose <- Rc.int value
-    | "max_processes" -> c.max_running_processes <- Rc.int value
-    | "default_editor" -> c.default_editor <- Rc.string value
-    | s ->
-        eprintf "Warning: ignore unknown key [%s] in whyide config file@." s
 
+type ide = {
+  ide_window_width : int;
+  ide_window_height : int;
+  ide_tree_width : int;
+  ide_task_height : int;
+  ide_verbose : int;
+  ide_default_editor : string;
+}
 
+let default_ide =
+  { ide_window_width = 1024;
+    ide_window_height = 768;
+    ide_tree_width = 512;
+    ide_task_height = 384;
+    ide_verbose = 0;
+    ide_default_editor = "";
+  }
+
+let load_ide section =
+  { ide_window_width =
+      get_int section ~default:default_ide.ide_window_width "window_width";
+    ide_window_height =
+      get_int section ~default:default_ide.ide_window_height "window_height";
+    ide_tree_width =
+      get_int section ~default:default_ide.ide_tree_width "tree_width";
+    ide_task_height =
+      get_int section ~default:default_ide.ide_task_height "task_height";
+    ide_verbose =
+      get_int section ~default:default_ide.ide_verbose "verbose";
+    ide_default_editor =
+      get_string section ~default:default_ide.ide_default_editor
+        "default_editor";
+  }
 
 let get_prover_data env id pr acc =
   try
@@ -61,17 +82,22 @@ let get_prover_data env id pr acc =
     acc
 
 let load_config config =
-    let env = Env.create_env (Lexer.retrieve config.main.loadpath) in
-    { window_height = config.ide.Whyconf.window_height;
-      window_width  = config.ide.Whyconf.window_width;
-      tree_width    = config.ide.Whyconf.tree_width;
-      task_height   = config.ide.Whyconf.task_height;
-      time_limit    = config.main.Whyconf.timelimit;
-      mem_limit     = config.main.Whyconf.memlimit;
-      verbose       = config.ide.Whyconf.verbose;
-      max_running_processes = config.main.Whyconf.running_provers_max;
-      provers = Mstr.fold (get_prover_data env) config.Whyconf.provers [];
-      default_editor = config.ide.Whyconf.default_editor;
+  let main = get_main config in
+  let ide  = match get_section config.Whyconf.config "ide" with
+    | None -> default_ide
+    | Some s -> load_ide s in
+  let provers = get_provers config in
+  let env = Env.create_env (Lexer.retrieve main.loadpath) in
+    { window_height = ide.ide_window_height;
+      window_width  = ide.ide_window_width;
+      tree_width    = ide.ide_tree_width;
+      task_height   = ide.ide_task_height;
+      time_limit    = main.Whyconf.timelimit;
+      mem_limit     = main.Whyconf.memlimit;
+      verbose       = ide.ide_verbose;
+      max_running_processes = main.Whyconf.running_provers_max;
+      provers = Mstr.fold (get_prover_data env) provers [];
+      default_editor = ide.ide_default_editor;
       config         = config;
       env            = env
     }
@@ -92,24 +118,23 @@ let save_config t =
         editor  = pr.editor;
       } acc in
   let config = t.config in
-  let main = { config.main with
-    Whyconf.timelimit    = t.time_limit;
-    memlimit     = t.mem_limit;
-    running_provers_max = t.max_running_processes;
-  } in
-  let ide = {
-    Whyconf.window_height = t.window_height;
-    window_width = t.window_width;
-    tree_width   = t.tree_width;
-    task_height  = t.task_height;
-    verbose  = t.verbose;
-    default_editor = t.default_editor;
-  } in
-  let config = {config with
-    Whyconf.provers = List.fold_left save_prover Mstr.empty t.provers;
-    main    = main;
-    ide     = ide;
-  } in
+  let config = set_main config
+    { (get_main config) with
+      timelimit    = t.time_limit;
+      memlimit     = t.mem_limit;
+      running_provers_max = t.max_running_processes;
+    } in
+  let ide = empty_section in
+  let ide = set_int ide "window_height" t.window_height in
+  let ide = set_int ide "window_width" t.window_width in
+  let ide = set_int ide "tree_width" t.tree_width in
+  let ide = set_int ide "task_height" t.task_height in
+  let ide = set_int ide "verbose" t.verbose in
+  let ide = set_string ide "default_editor" t.default_editor in
+  let rc = set_section config.Whyconf.config "ide" ide in
+  let config = {config with Whyconf.config = rc} in
+  let config = set_provers config
+    (List.fold_left save_prover Mstr.empty t.provers) in
   save_config config
 
 (*
@@ -287,19 +312,8 @@ let preferences c =
   dialog#destroy ()
 
 let run_auto_detection gconfig =
-  let config2 = run_auto_detection gconfig.config in
-  let gconfig2 = load_config config2 in
-  gconfig.window_width <- gconfig2.window_width;
-  gconfig.window_height <- gconfig2.window_height;
-  gconfig.tree_width <- gconfig2.tree_width;
-  gconfig.task_height <- gconfig2.task_height;
-  gconfig.time_limit <- gconfig2.time_limit;
-  gconfig.mem_limit <- gconfig2.mem_limit;
-  gconfig.verbose <- gconfig2.verbose;
-  gconfig.max_running_processes <- gconfig2.max_running_processes;
-  gconfig.provers <- gconfig2.provers;
-  gconfig.default_editor <- gconfig2.default_editor;
-  gconfig.config <- gconfig2.config
+  let provers = run_auto_detection () in
+  gconfig.provers <- Mstr.fold (get_prover_data gconfig.env) provers [];
 
 (*
 Local Variables: 

src/main.ml

@@ -224,7 +224,8 @@ let () =
     let config = read_config !opt_config in
     let print fmt s prover = fprintf fmt "%s (%s)@\n" s prover.name in
     let print fmt m = Mstr.iter (print fmt) m in
-    printf "@[<hov 2>Known provers:@\n%a@]@." print config.provers
+    let provers = get_provers config in
+    printf "@[<hov 2>Known provers:@\n%a@]@." print provers
   end;
   if !opt_list_metas then begin
     opt_list := true;
@@ -291,12 +292,13 @@ let () =
     default_config
   in
 
-  opt_loadpath := List.rev_append !opt_loadpath config.main.loadpath;
-  if !opt_timelimit = None then opt_timelimit := Some config.main.timelimit;
-  if !opt_memlimit  = None then opt_memlimit  := Some config.main.memlimit;
+  let main = get_main config in
+  opt_loadpath := List.rev_append !opt_loadpath main.loadpath;
+  if !opt_timelimit = None then opt_timelimit := Some main.timelimit;
+  if !opt_memlimit  = None then opt_memlimit  := Some main.memlimit;
   begin match !opt_prover with
   | Some s ->
-      let prover = try Mstr.find s config.provers with
+      let prover = try Mstr.find s (get_provers config) with
         | Not_found -> eprintf "Driver %s not found.@." s; exit 1
       in
       opt_command := Some prover.command;

src/util/pp.ml

@@ -58,13 +58,22 @@ let print_iter1 iter sep print fmt l =
 
 let print_iter2 iter sep1 sep2 print1 print2 fmt l =
   let first = ref true in
-  iter (fun x y -> 
+  iter (fun x y ->
           if !first
           then first := false
-          else sep1 fmt (); 
+          else sep1 fmt ();
           print1 fmt x;sep2 fmt (); print2 fmt y) l
 
 
+let print_iter22 iter sep print fmt l =
+  let first = ref true in
+  iter (fun x y ->
+          if !first
+          then first := false
+          else sep fmt ();
+          print fmt x y) l
+
+
 let print_pair_delim start sep stop pr1 pr2 fmt (a,b) =
   fprintf fmt "%a%a%a%a%a" start () pr1 a sep () pr2 b stop ()
 

src/util/pp.mli

@@ -55,13 +55,28 @@ val print_iter1 :
   (Format.formatter -> 'a -> unit) -> 
   Format.formatter -> 'b -> unit
 
-val print_iter2: 
+val print_iter2:
   (('a -> 'b -> unit) -> 'c -> unit) ->
   (Format.formatter -> unit -> unit) ->
   (Format.formatter -> unit -> unit) ->
-  (Format.formatter -> 'a -> unit) -> 
-  (Format.formatter -> 'b -> unit) -> 
+  (Format.formatter -> 'a -> unit) ->
+  (Format.formatter -> 'b -> unit) ->
+  Format.formatter -> 'c -> unit
+(**  [print_iter2 iter sep1 sep2 print1 print2 fmt t]
+     iter iterator on [t : 'c]
+     print1 k sep2 () print2 v sep1 () print1  sep2 () ...
+*)
+
+val print_iter22:
+  (('a -> 'b -> unit) -> 'c -> unit) ->
+  (Format.formatter -> unit -> unit) ->
+  (Format.formatter -> 'a -> 'b -> unit) ->
   Format.formatter -> 'c -> unit
+(**  [print_iter22 iter sep print fmt t]
+     iter iterator on [t : 'c]
+     print k v sep () print k v sep () ...
+*)
+
 
 val space : formatter -> unit -> unit
 val alt : formatter -> unit -> unit

src/util/rc.mli

@@ -18,31 +18,117 @@
 (**************************************************************************)
 
 (** Parse rc files *)
-type rc_value =
-  | RCint of int
-  | RCbool of bool
-  | RCfloat of float
-  | RCstring of string
-  | RCident of string
+exception Bad_value_type of string * string * string
+(** key * expected * found *)
+exception Key_not_found of string
+(** key *)
+exception Multiple_value of string
+(** key *)
+exception Yet_defined_key of string
+(** key *)
+exception Multiple_section of string
+exception Section_b_family of string
+exception Family_two_many_args of string
+exception Not_exhaustive of  string
+exception Yet_defined_section of string
+(** key *)
 
-type t = (string list * (string * rc_value) list) list
 
-val int : rc_value -> int
-  (** raise Failure "Rc.int" if not a int value *)
+type t
+type section
+type family  = (string * section) list
 
-val bool : rc_value -> bool
-  (** raise Failure "Rc.bool" if not a int value *)
+val empty : t
+val empty_section : section
 
-val string : rc_value -> string
-  (** raise Failure "Rc.string" if not a string or an ident value *)
+val get_section : t -> string -> section option
+(** return None if the section is not in the rc file *)
+val get_family  : t -> string -> family
+
+val set_section : t -> string -> section -> t
+val set_family  : t -> string -> family  -> t
+
+val get_int  : ?default:int      -> section -> string -> int
+  (** raise Bad_value_type
+      raise Key_not_found
+      raise Multiple_value
+  *)
+
+val get_intl : ?default:int list -> section -> string -> int list
+  (** raise Bad_value_type
+      raise Key_not_found *)
+
+val set_int : section -> string -> int -> section
+  (** raise Yet_defined_key *)
+
+val set_intl : section -> string -> int list -> section
+  (** raise Yet_defined_key *)
+
+val get_bool  : ?default:bool       -> section -> string -> bool
+  (** raise Bad_value_type
+      raise Key_not_found
+      raise Multiple_value
+  *)
+
+val get_booll  : ?default:bool list -> section -> string -> bool list
+  (** raise Bad_value_type
+      raise Key_not_found *)
+
+val set_bool : section -> string -> bool -> section
+  (** raise Yet_defined_key *)
+
+val set_booll : section -> string -> bool list -> section
+  (** raise Yet_defined_key *)
+
+
+val get_string  : ?default:string      -> section -> string -> string
+  (** raise Bad_value_type
+      raise Key_not_found
+      raise Multiple_value
+  *)
+
+val get_stringl : ?default:string list -> section -> string -> string list
+  (** raise Bad_value_type
+      raise Key_not_found *)
+
+val set_string : section -> string -> string -> section
+  (** raise Yet_defined_key *)
+
+val set_stringl : section -> string -> string list -> section
+  (** raise Yet_defined_key *)
+
+
+
+(* val ident  : ?default:string      -> section -> string -> string *)
+(*   (\** raise Bad_value_type *)
+(*       raise Key_not_found *)
+(*       raise Multiple_value *)
+(*   *\) *)
+
+(* val identl : ?default:string list -> section -> string -> string list *)
+(*   (\** raise Bad_value_type *)
+(*       raise Key_not_found *\) *)
+
+(* val set_ident : section -> string -> string -> section *)
+(*   (\** raise Yet_defined_key *)
+(*       raise Bad_value_type *)
+(*   *\) *)
+
+(* val set_identl : section -> string -> string list -> section *)
+(*   (\** raise Yet_defined_key *)
+(*       raise Bad_value_type *)
+(*   *\) *)
+
+val check_exhaustive : section -> Util.Sstr.t -> unit
+  (**  raise Not_exhaustive of string *)
 
 val from_file : string -> t
   (** returns the records of the file [f]
-      @raise Not_found is f does not exists 
+      @raise Not_found is f does not exists
       @raise Failure "lexing" in case of incorrect syntax *)
 
 val to_file   : string -> t -> unit
-  (** save the records in the filr [f] *)
+  (** [to_file f t] save the records [t] in the file [f] *)
 
 val get_home_dir : unit -> string
   (** returns the home dir of the user *)

src/util/rc.mll

@@ -20,6 +20,7 @@
 {
 
   open Lexing
+  open Util
 
   let get_home_dir () =
     try Sys.getenv "HOME"
@@ -28,6 +29,19 @@
       try Sys.getenv "USERPROFILE"
       with Not_found -> ""
 
+exception Bad_value_type of string * string * string
+(** key * expected * found *)
+exception Key_not_found of string
+(** key *)
+exception Multiple_value of string
+(** key *)
+exception Multiple_section of string
+exception Section_b_family of string
+exception Family_two_many_args of string
+exception Not_exhaustive of  string
+exception Yet_defined_section of string
+exception Yet_defined_key of string
+
 type rc_value =
   | RCint of int
   | RCbool of bool
@@ -35,20 +49,122 @@ type rc_value =
   | RCstring of string
   | RCident of string
 
-type t = (string list * (string * rc_value) list) list
+type section = rc_value list Mstr.t
+type family  = (string * section) list
+type ofamily  = (string option * section) list
+type t = ofamily Mstr.t
+
+let empty = Mstr.empty
+let empty_section = Mstr.empty
+
+let make_t tl =
+  let add_key acc (key,value) =
+    let l = try Mstr.find key acc with Not_found -> [] in
+    Mstr.add key (value::l) acc in
+  let add_section t (args,sectionl) =
+    let sname,arg = match args with
+      | []    -> assert false
+      | [sname]    -> sname,None
+      | [sname;arg] -> sname,Some arg
+      | sname::_     -> raise (Family_two_many_args sname) in
+    let m = List.fold_left add_key empty_section sectionl in
+    let m = Mstr.map List.rev m in
+    let l = try Mstr.find sname t with Not_found -> [] in
+    Mstr.add sname ((arg,m)::l) t in
+  List.fold_left add_section empty tl
+
+let get_section t sname =
+  try
+    let l = Mstr.find sname t in
+    match l with
+      | [None,v] -> Some v
+      | [Some _,_] -> raise (Section_b_family sname)
+      | _ -> raise (Multiple_section sname)
+  with Not_found -> None
+
+let get_family t sname =
+  try
+    let l = Mstr.find sname t in
+    let get (arg,section) =
+      (match arg with None -> raise (Section_b_family sname) | Some v -> v,
+        section) in
+    List.map get l
+  with Not_found -> []
+
+
+let set_section t sname section =
+  Mstr.add sname [None,section] t
+
+let set_family t sname sections =
+  if sections = [] then Mstr.remove sname t else
+    let set (arg,section) = (Some arg,section) in
+    Mstr.add sname (List.map set sections) t
+
+let get_value read ?default section key =
+  try
+    let l = Mstr.find key section in
+    match l with
+      | [v] -> read v
+      | _ -> raise (Multiple_value key)
+  with Not_found ->
+    match default with
+      | None -> raise (Key_not_found key)
+      | Some v -> v
+
+let get_valuel read ?default section key =
+  try
+    let l = Mstr.find key section in
+    List.map read l
+  with Not_found ->
+    match default with
+      | None -> raise (Key_not_found key)
+      | Some v -> v
 
-let int = function
+let set_value write section key value =
+  Mstr.add key [write value] section
+
+let set_valuel write section key valuel =
+  if valuel = [] then Mstr.remove key section else
+    Mstr.add key (List.map write valuel) section
+
+let rint = function
   | RCint n -> n
   | _ -> failwith "Rc.int"
 
-let bool = function
+let wint i = RCint i
+
+let rbool = function
   | RCbool b -> b
   | _ -> failwith "Rc.bool"
 
-let string = function
+let wbool b = RCbool b
+
+let rstring = function
   | RCident s | RCstring s -> s
   | _ -> failwith "Rc.string"
 
+let wstring s = RCstring s
+
+let get_int = get_value rint
+let get_intl = get_valuel rint
+let set_int = set_value wint
+let set_intl = set_valuel wint
+
+let get_bool = get_value rbool
+let get_booll = get_valuel rbool
+let set_bool = set_value wbool
+let set_booll = set_valuel wbool
+
+let get_string = get_value rstring
+let get_stringl = get_valuel rstring
+let set_string = set_value wstring
+let set_stringl = set_valuel wstring
+
+let check_exhaustive section keyl =
+  let test k _ = if Sstr.mem k keyl then ()
+    else raise (Not_exhaustive k) in
+  Mstr.iter test section
+
 let buf = Buffer.create 17
 
 let current_rec = ref []
@@ -161,25 +277,30 @@ and string_val key = parse
       let lb = from_channel c in
       record lb;
       close_in c;
-      List.rev !current
+      make_t !current
 
 open Format
 
-let to_file s l =
+let to_file s t =
   let print_value fmt = function
       | RCint i -> pp_print_int fmt i
       | RCbool b -> pp_print_bool fmt b
       | RCfloat f -> pp_print_float fmt f
-      | RCstring s -> fprintf fmt "\"%S\"" s
+      | RCstring s -> fprintf fmt "%S" s
       | RCident s -> pp_print_string fmt s in
-  let print_kv fmt (k,v) = fprintf fmt "%s = %a" k print_value v in
-  let print_section fmt (h,l) =
-    fprintf fmt "[%a]@\n%a"
-      (Pp.print_list Pp.space pp_print_string) h
-      (Pp.print_list Pp.newline print_kv) l in
+  let print_kv k fmt v = fprintf fmt "%s = %a" k print_value v in
+  let print_kvl fmt k vl = Pp.print_list Pp.newline (print_kv k) fmt vl in
+  let print_section sname fmt (h,l) =
+    fprintf fmt "[%s %a]@\n%a"
+      sname (Pp.print_option Pp.string) h
+      (Pp.print_iter22 Mstr.iter Pp.newline2 print_kvl) l in
+  let print_sectionl fmt sname l =
+    Pp.print_list Pp.newline (print_section sname) fmt l in
+  let print_t fmt t =
+    Pp.print_iter22 Mstr.iter Pp.newline2 print_sectionl fmt t in
   let out = open_out s in
   let fmt = formatter_of_out_channel out in
-  Pp.print_list Pp.newline print_section fmt l;
+  print_t fmt t;
   pp_print_flush fmt ();
   close_out out