a little enhancement in Rc to make config syntax prettier

src/driver/whyconf.ml

@@ -24,6 +24,8 @@ open Util
 
 type error =
   | SyntaxError
+  | ExtraParameters of string
+  | MissingParameters of string
   | UnknownSection of string
   | UnknownField of string
   | MissingSection of string
@@ -51,6 +53,10 @@ let print_rc_value fmt = function
 let report fmt = function
   | SyntaxError ->
       fprintf fmt "syntax error"
+  | ExtraParameters s ->
+      fprintf fmt "section '%s': header too long" s
+  | MissingParameters s ->
+      fprintf fmt "section '%s': header too short" s
   | UnknownSection s ->
       fprintf fmt "unknown section '%s'" s
   | UnknownField s ->
@@ -79,9 +85,9 @@ let report fmt = function
 (* Configuration file *)
 
 type config_prover = {
-  description : string;     (* "Alt-Ergo v2.95 (special)" *)
+  name    : string;   (* "Alt-Ergo v2.95 (special)" *)
   command : string;   (* "exec why-limit %t %m alt-ergo %f" *)
-  driver_file : string;     (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
+  driver  : string;   (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
 }
 
 type config = {
@@ -120,27 +126,20 @@ let get_field f = function
   | None -> error (MissingField f)
   | Some v -> v
 
-let load_prover provers al =
+let load_prover al =
   let nam = ref None in
-  let dsc = ref None in
   let cmd = ref None in
   let drv = ref None in
   let load (key, value) = match key with
-    | "name"        -> set_ident key nam value
-    | "description" -> set_string key dsc value
+    | "name"        -> set_string key nam value
     | "command"     -> set_string key cmd value
     | "driver"      -> set_string key drv value
     | _             -> error (UnknownField key)
   in
   List.iter load al;
-  let prover = {
-    description = get_field "description" !dsc;
+  { name    = get_field "name" !nam;
     command = get_field "command" !cmd;
-    driver_file = get_field "driver"      !drv }
-  in
-  let n = get_field "name" !nam in
-  if Mstr.mem n provers then error (DuplicateProver n);
-  Mstr.add n prover provers
+    driver  = get_field "driver" !drv }
 
 let load_main main al =
   let lp = ref [] in
@@ -181,10 +180,17 @@ let read_config ?conf_file () =
   let provers = ref Mstr.empty in
   let have_main = ref false in
   let load (key, al) = match key with
-    | "main" when !have_main -> error (DuplicateSection key)
-    | "main" -> main := load_main !main al
-    | "prover" -> provers := load_prover !provers al
-    | _ -> error (UnknownSection key)
+    | "main" :: rest ->
+        if rest <> [] then error (ExtraParameters "main");
+        if !have_main then error (DuplicateSection "main");
+        main := load_main !main al
+    | "prover" :: name :: rest ->
+        if rest <> [] then error (ExtraParameters ("prover " ^ name));
+        if Mstr.mem name !provers then error (DuplicateProver name);
+        provers := Mstr.add name (load_prover al) !provers
+    | "prover" :: [] -> error (MissingParameters "prover")
+    | s :: _ -> error (UnknownSection s)
+    | [] -> assert false
   in
   List.iter load rc;
   { !main with provers = !provers }
@@ -198,11 +204,10 @@ let save_config config =
   Util.option_iter (fprintf fmt "memlimit = %d@\n") config.memlimit;
   fprintf fmt "@.";
   let print_prover name prover =
-    fprintf fmt "[prover]@\n";
-    fprintf fmt "name = %s@\n" name;
-    fprintf fmt "description = \"%s\"@\n" prover.description;
+    fprintf fmt "[prover %s]@\n" name;
+    fprintf fmt "name = \"%s\"@\n" prover.name;
     fprintf fmt "command = \"%s\"@\n" prover.command;
-    fprintf fmt "driver = \"%s\"@\n@." prover.driver_file;
+    fprintf fmt "driver = \"%s\"@\n@." prover.driver;
   in
   Mstr.iter print_prover config.provers;
   close_out ch

src/driver/whyconf.mli

@@ -20,9 +20,9 @@
 open Util
 
 type config_prover = {
-  description : string;     (* "Alt-Ergo v2.95 (special)" *)
+  name    : string;   (* "Alt-Ergo v2.95 (special)" *)
   command : string;   (* "exec why-limit %t %m alt-ergo %f" *)
-  driver_file : string;     (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
+  driver  : string;   (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
 }
 
 type config = {

src/manager/test.ml

@@ -5,24 +5,24 @@ open Whyconf
 
 let autodetection () = 
   let alt_ergo = {
-    description = "Alt-Ergo";
+    name    = "Alt-Ergo";
     command = "alt-ergo %s";
-    driver_file = "drivers/alt_ergo.drv" }
+    driver  = "drivers/alt_ergo.drv" }
   in
   let z3 = {
-    description = "Z3";
+    name    = "Z3";
     command = "z3 -smt -in";
-    driver_file = "drivers/z3.drv" }
+    driver  = "drivers/z3.drv" }
   in
   let cvc3 = {
-    description = "CVC3";
+    name    = "CVC3";
     command = "cvc3 -lang smt";
-    driver_file = "drivers/cvc3.drv" }
+    driver  = "drivers/cvc3.drv" }
   in
   let coq = {
-    description = "Coq";
+    name    = "Coq";
     command = "coqc %s";
-    driver_file = "drivers/coq.drv" }
+    driver  = "drivers/coq.drv" }
   in
   let provers = Util.Mstr.empty in
   let provers = Util.Mstr.add "alt-ergo" alt_ergo provers in

src/util/rc.mli

@@ -42,7 +42,7 @@ val bool : rc_value -> bool
 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
+val from_file : string -> (string list * (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 *)

src/util/rc.mll

@@ -57,7 +57,7 @@ let string = function
 
 let buf = Buffer.create 17
 
-let current_rec = ref ""
+let current_rec = ref []
 let current_list = ref []
 let current = ref []
 
@@ -67,7 +67,7 @@ let push_field key value =
 let push_record () =
   if !current_list <> [] then
     current := (!current_rec,List.rev !current_list) :: !current;
-  current_rec := "";
+  current_rec := [];
   current_list := []
 
 }
@@ -85,11 +85,8 @@ let escape = ['\\''"''n''t''r']
 rule record = parse
   | space 
       { record lexbuf }
-  | '[' (ident as key) ']'  
-      { push_record();
-	current_rec := key;
-	record lexbuf 
-      }
+  | '[' (ident as key) space*
+      { header [key] lexbuf }
   | eof 
       { push_record () }
   | (ident as key) space* '=' space* 
@@ -97,6 +94,18 @@ rule record = parse
   | _ as c
       { failwith ("Rc: invalid keyval pair starting with " ^ String.make 1 c) }
 
+and header keylist = parse
+  | (ident as key) space*
+      { header (key::keylist) lexbuf }
+  | ']'
+      { push_record ();
+        current_rec := List.rev keylist;
+        record lexbuf }
+  | eof
+      { failwith "Rc: unterminated header" }
+  | _ as c
+      { failwith ("Rc: invalid header starting with " ^ String.make 1 c) }
+
 and value key = parse
   | integer as i
       { push_field key (RCint (int_of_string i));
@@ -116,10 +125,10 @@ and value key = parse
   | 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" }
+  | _ as c
+      { failwith ("Rc: invalid value starting with " ^ String.make 1 c) }
 
 and string_val key = parse 
   | '"' 

why.conf

@@ -2,27 +2,23 @@
 loadpath = "theories"
 timelimit = 10
 
-[prover]
-name = alt-ergo
-description = "Alt-Ergo"
+[prover alt-ergo]
+name = "Alt-Ergo"
 command = "alt-ergo %s"
 driver = "drivers/alt_ergo.drv"
 
-[prover]
-name = coq
-description = "Coq"
+[prover coq]
+name = "Coq"
 command = "coqc %s"
 driver = "drivers/coq.drv"
 
-[prover]
-name = cvc3
-description = "CVC3"
+[prover cvc3]
+name = "CVC3"
 command = "cvc3 -lang smt"
 driver = "drivers/cvc3.drv"
 
-[prover]
-name = z3
-description = "Z3"
+[prover z3]
+name = "Z3"
 command = "z3 -smt -in"
 driver = "drivers/z3.drv"